module edt

//Cette conception est une "abstraction" de la réalité pour réduire l'explosion combinatoire.
//Pour une plage donnée, Alloy peut renvoyer un ensemble d'affectations de groupes 
//avec des types de cours et enseignants differents mais il ne précise pas qui assure quel groupe dans cette plage  

//Donc, la source d'explosion combinatoire est d'avoir plusieurs ensembles "composés"
//Dans la conception actuelle, "PlageHoraie" est le seul ensemble composé  


abstract sig PlageHoraire{
  occupee  : set Groupe,  //une plage peut ête affectée à plusieurs groupes
  type : set TypeCours,
  intitule : set NomCours,
  assuree : set Enseignant,
  appartient : set Jour,
  precedeP : set PlageHoraire,
  avantP : set PlageHoraire
  //seDeroule : set Salle
}

//introduire un ensemble
abstract sig Jour {}

abstract sig NomCours {}
 
abstract sig Enseignant {
  //prend : PlageHoraire
}

abstract sig Groupe {}

abstract sig TypeCours {}

one sig p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20  extends PlageHoraire{}
one sig jour1, jour2, jour3, jour4, jour5 extends Jour{}
one sig en_1, en_2, en_3, en_4, en_5, en_6, en_7, en_8, en_9, en_10, en_11, e_12, en_13, en_14, en_15, e_16    extends Enseignant{}
one sig info, maths, com, gestion, anglais, info2, info3, info4  extends NomCours{}
one sig CM, TD, TP   extends TypeCours{}
one sig g1, g2, g3, g4, g5 extends Groupe{}

//chaque plage est occupee par au plus 4 groupes et au moins 1 groupe
//Le nb d'affectations est égal au nb d'enseignants
fact  { 
 all p : PlageHoraire |  #p.occupee < 5 && #p.occupee > 0   && #p.occupee = #p.assuree 
}

//pour chaque plage, le nb d'affectations de groupe > le nb de types de cours et d'intitules 
fact {
   all p : PlageHoraire | #p.occupee >= #p.type &&  #p.occupee >= #p.intitule 
}
 
//Pour une plage,  il y a au moins un type de cours, un intitule
fact {
   all p : PlageHoraire | #p.occupee > 0 => #p.type >0  && #p.intitule >0 && #p.assuree > 0  
}


//la relation "prend" est l'inverse de "assure"
//fact  { 
// all en : Enseignant,  p : PlageHoraire  | (p->en in assuree) => (en->p in prend)
//}

//  la relation "prend" est l'inverse de "assure"
//fact   { 
// all en : Enseignant, p : PlageHoraire  |  (en->p in prend) => (p->en in assuree)
//}

//chaque plage appartient à un seul jour
fact toutePlageAppartientAUnJour { 
 all p : PlageHoraire | one j : Jour | p->j in appartient
}

//  pour chaque Enseignant, il assure au moins 1 plage au plus 20
//fact {
// all en : Enseignant  |  #en.prend < 20  && #en.prend > 0
//}

//lister les instances de la relation "appartient" et "predecedP"
fact{
p1.appartient=jour1 && 
p2.appartient=jour1 && p1->p2 in precedeP &&
p3.appartient=jour1 && p2->p3 in precedeP &&
p4.appartient=jour1 && p3->p4 in precedeP &&

p5.appartient=jour2 && p4->p5 in precedeP &&
p6.appartient=jour2 && p5->p6 in precedeP &&
p7.appartient=jour2 && p6->p7 in precedeP &&
p8.appartient=jour2 && p7->p8 in precedeP &&

p9.appartient=jour3 && p8->p9 in precedeP &&
p10.appartient=jour3 && p9->p10 in precedeP &&
p11.appartient=jour3 && p10->p11 in precedeP &&
p12.appartient=jour3 && p11->p12 in precedeP &&

p13.appartient=jour4 && p12->p13 in precedeP &&
p14.appartient=jour4 && p13->p14 in precedeP &&
p15.appartient=jour4 && p14->p15 in precedeP &&
p16.appartient=jour4 && p15->p16 in precedeP &&

p17.appartient=jour5 && p16->p17 in precedeP &&
p18.appartient=jour5 && p17->p18 in precedeP &&
p19.appartient=jour5 && p18->p19 in precedeP &&
p20.appartient=jour5 && p19->p20 in precedeP 
}
 
//non reflexif sur l'ordre de plages
fact unePlageNeSePrecedePas{
all p : PlageHoraire | p->p not in precedeP
}

 
//non inversable sur l'ordre de plages
fact {
 all v1_p, v2_p : PlageHoraire | v1_p -> v2_p in precedeP => v2_p -> v1_p not in precedeP
}

//contrainte pour la consecutivite
fact {
 all  v1_p, v2_p, v3_p : PlageHoraire | (v1_p->v3_p in precedeP && v2_p->v3_p in precedeP) => (v1_p= v2_p)
}

//  pour chaque Enseignant, il ne peut pas assurer deux plages consécutives 
fact {
 all en : Enseignant,  v1_p, v2_p : PlageHoraire  | v1_p->en in assuree && v2_p->en in assuree  => (v1_p->v2_p not in precedeP) && (v2_p->v1_p not in precedeP)
}


//pour trois plages v1_p, v2_p, v3_p, et pour un nom de cours qui occupe 3 plages, si ce nom de cours
// a lieu avec trois modalites alors CM > TD >TP
fact   { 
 all v1_p, v2_p, v3_p : PlageHoraire, v1_g, v2_g,  v3_g  : Groupe | v1_p->v1_g in occupee && v2_p->v2_g in occupee && v3_p->v3_g in occupee
    && (v1_p.type=CM) && (v2_p.type=TD) && (v3_p.type=TP) => (v1_p->v2_p in *precedeP ) && (v2_p->v3_p in *precedeP)    
}

//pour chaque plage horaire, si elle a type CM pour un groupe allors elle ne peut pas avoir en meme temps d'autres TD ou TP, 
//plusieurs intitulés 
fact  {
 all p : PlageHoraire, v1_g,  v2_g  : Groupe, t1, t2 : TypeCours , n1, n2 : NomCours  |  ( p->v1_g in occupee && p->v2_g in occupee &&
       p->t1 in type && p->t2 in type && t1 = CM  && p->n1 in intitule && p->n2 in intitule )
      =>  t2 = t1 && n1= n2  
}

//pour chaque plage horaire, si elle a type CM pour un groupe allors elle ne peut que avoir un seul
//enseignants. Attention : le temps de réponse sera important si le nb d'enseignants > 10 
//fact  {
// all p : PlageHoraire, v1_g,  v2_g  : Groupe, t1, t2 : TypeCours   e1, e2 :Enseignant |  ( p->v1_g in occupee && p->v2_g in occupee &&
//      p->e1 in assuree && p->e2 in assuree && p->t1 in type && p->t2 in type && t1 = CM  )
//      =>  t2 = t1 && e1=e2
//}
 
//chaque NomCours doit avoir une plage CM
fact {
 all nc : NomCours | some p : PlageHoraire, g : Groupe  | p->g in occupee && p->nc in intitule && p.type = CM
}

//chaque NomCours doit avoir une plage TD
fact {
 all nc : NomCours | some p : PlageHoraire, g : Groupe | p->g in occupee && p->nc in intitule  &&  p.type = TD
}
 
//chaque NomCours doit avoir une plage TP
fact {
 all nc : NomCours | some p : PlageHoraire, g : Groupe | p->g in occupee && p->nc in intitule  &&  p.type = TP
}

//si une plage a le type CM alors elle est occuppe par un seul cours  => INCONSISTENT ???
//fact {
//  all vp : PlageHoraire, g : Groupe | (vp->g in occupee && vp.type = CM) => one vp.affectee
//}

//l'enseignant e1 ne peut pas assurer le cours CM anglais
fact {
  all p : PlageHoraire | p->en_1 in assuree && p->anglais in intitule && p->CM in type => 
       (some e1 : Enseignant | e1 !=en_1 &&  p->e1 in assuree)
}
 
//l'enseignant en_2 ne peut pas assurer le cours CM gestion
fact {
  all p : PlageHoraire | p->en_2 in assuree && p->gestion in intitule && p->CM in type => 
       (some e1 : Enseignant | e1 !=en_2 &&  p->e1 in assuree)
}

//l'enseignant en_3 ne peut pas assurer le cours CM info
fact {
  all p : PlageHoraire | p->en_3 in assuree && p->info in intitule && p->CM in type => 
       (some e1 : Enseignant | e1 !=en_3 &&  p->e1 in assuree)
}

//l'enseignant en_4 ne peut pas assurer le TP info
fact {
  all p : PlageHoraire | p->en_4 in assuree && p->info in intitule && p->TP in type => 
       (some e1 : Enseignant | e1 !=en_4 &&  p->e1 in assuree)
}

run {}

